$\forall$${\it es}$:event\_system\{i:l\}, ${\it e'}$,$e$,$a$:es{-}E(${\it es}$).
\\[0ex](es{-}locl(${\it es}$; $e$; $a$) $\wedge$ es{-}le(${\it es}$; $a$; ${\it e'}$))
\\[0ex]$\Rightarrow$ ([$e$, ${\it e'}$] = append([$e$, es{-}pred(${\it es}$; $a$)]; [$a$, ${\it e'}$]) $\in$ (es{-}E(${\it es}$) List))